es:event_system{i:l}, x:Id, e:es-E(es).
((es-first(es; e)))
 (es-isconst(es; loc(e); x))
 (es-after(es; x; es-pred(es; e)) = es-when(es; x; e)  es-vartype(es; loc(e); x)) 

latex

Definitions

, t  T, x:AB(x), x:A. B(x), P  Q, Id, es-E(es), es-first(es; e), b, A, loc(e), es-isconst(es; i; x), es-when(es; x; e), es-after(es; x; e), <a, b>, es-vartype(es; i; x), s = t, x:A  B(x), P  Q, event_system{i:l}, #$n, , prop{i:l}, sqequal(s; t), guard(T), sq_type(T), f(a), es-time(es; e), r - s, r + s, es_state_after(es; e), trans(T; x,y.E(x;y)), x:A. B(x), SWellFounded(R(x;y)), atom{$n:n}, let x,y = A in B(x;y), t.1, False, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , es-state-ap(s; x), es-pred(es; e)

Lemmas

subtype rel self, es-isconst-property, Id sq, es-loc-pred, qadd wf, qsub wf, es-time wf, es-pred wf, es-vartype wf, es-after wf, event system wf, es-axioms, es-isconst wf, es-loc wf, not wf, assert wf, es-first wf, es-E wf, Id wf, int inc rationals